the_es:ES, e:E. valtype(e)  Type 

latex

Definitions	E, ES, valtype(e), Unit, P  Q, P & Q, isrcv(e), rcvtype(e), , Prop, b, A, b, t  T, acttype(e), x:A. B(x), P  Q
Lemmas	es-acttype wf, assert wf, not wf, bnot wf, es-rcvtype wf, bool wf, es-isrcv wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, event system wf, es-E wf